Hum. I'm a bit confused. I didn't mean to create a new issue along with the pull request, but I'm not sure if it was possible to create a pull request without the issue either. Sorry if this was avoidable.

[edit: I now figure that since there already was an issue for the change, which I was referencing (and closing) from the commit message, there was probably no need in creating an actual pull request, although I'm not sure if having a "native" pull request gives you significant workflow advantages or not. For a trivial change like this, I'd guess probably not.

If I could go back in time, I'd just do the referencing-from-the-commit thing, as it's less disruptive than having 2 separate issues. Lesson learned... Again, sorry for the noise.]

[edit2: Ok, re-reading #663 you did specifically ask for a pull request, so it's safe to assume that's what you actually wanted. Sorry, it's 2AM and I'm exhausted from a wacky sleep pattern. 😵]